(declare-const x String)
(declare-const y String)
(declare-const r (RegEx String))
(declare-const s (RegEx String))
(declare-const b1 Bool)
; Characters (bitvectors of size 8)
(declare-const c1 Unicode)
; Predicates on characters
(declare-const p (Array Unicode Bool))

(echo "====== string in regex checks ======")

(echo "==== atomic cases ====")

(echo "== none, all ==")
(simplify (not (str.in_re "" re.empty)))
(simplify (not (str.in_re "" re.nostr)))
(simplify (str.in_re "" re.all))
(simplify (not (str.in_re "a" re.empty)))
(simplify (not (str.in_re "aba" re.empty)))
(simplify (not (str.in_re "a" re.nostr)))
(simplify (str.in_re "a" re.all))
(simplify (str.in_re "aba" re.all))

(echo "== from string  ==")
(simplify (str.in_re "" (str.to_re "")))
(simplify (not (str.in_re "" (str.to_re "a"))))
(simplify (str.in_re "a" (str.to_re "a")))
(simplify (not (str.in_re "a" (str.to_re ""))))
(simplify (not (str.in_re "aba" (str.to_re "a"))))
(simplify (not (str.in_re "a" (str.to_re "b"))))
(simplify (not (str.in_re "aba" (str.to_re "ab"))))

(echo "== character ranges ==")
(simplify (not (str.in_re "" re.allchar)))
(simplify (not (str.in_re "" (re.range "a" "a"))))
(simplify (not (str.in_re "" (re.range x x))))
(simplify (str.in_re "a" re.allchar))
(simplify (str.in_re "b" re.allchar))
(simplify (not (str.in_re "aba" re.allchar)))
(simplify (str.in_re "a" (re.range "a" "b")))
(simplify (str.in_re "b" (re.range "a" "b")))
(simplify (str.in_re "c" (re.range "c" "c")))
(simplify (not (str.in_re "c" (re.range "c" "b"))))
(simplify (not (str.in_re "c" (re.range "a" "b"))))
(simplify (not (str.in_re "aba" (re.range "a" "b"))))

(echo "== ranges and strings using character literal ==")
(simplify (str.in_re (_ char #x61) (str.to_re (_ char #x61))))
(simplify (str.in_re (_ char #x6) (re.range (_ char #x6) (_ char #x8))))
(simplify (str.in_re (_ char #x7) (re.range (_ char #x6) (_ char #x8))))
(simplify (str.in_re (_ char #x8) (re.range (_ char #x6) (_ char #x8))))
(simplify (not (str.in_re (_ char #x9) (re.range (_ char #x6) (_ char #x8)))))
(simplify (str.in_re (_ char #x9) (re.union (re.range (_ char #x9) (_ char #xD)) (str.to_re " "))))
(simplify (not (str.in_re (_ char #x8) (re.union (re.range (_ char #x9) (_ char #xD)) (str.to_re " ")))))
(simplify (not (str.in_re "" (re.union (re.range (_ char #x9) (_ char #xD)) (str.to_re " ")))))

(echo "== character predicates ==")
(simplify (not (str.in_re "" (re.of.pred p))))
(simplify (not (str.in_re "aba" (re.of.pred p))))
(simplify (str.in_re (_ char #x24) (re.of.pred (store p (_ Char #x24) true))))
(simplify (not (str.in_re (_ char #x24) (re.of.pred (store p (_ Char #x24) false)))))
(simplify (str.in_re (_ char #x24) (re.of.pred (store (store p (_ Char #x23) false) (_ Char #x24) true))))
(simplify (str.in_re (_ char #x24) (re.of.pred (store (store p (_ Char #x24) true) (_ Char #x24) true))))
(simplify (str.in_re (_ char #x24) (re.of.pred (store (store p (_ Char #x24) false) (_ Char #x24) true))))
(simplify (not (str.in_re (_ char #x24) (re.of.pred (store (store p (_ Char #x24) true) (_ Char #x24) false)))))
(simplify (str.in_re "a" (re.of.pred ((as const (Array Unicode Bool)) true))))
(simplify (not (str.in_re "a" (re.of.pred ((as const (Array Unicode Bool)) false)))))
(simplify (not (str.in_re (_ char #x24) (re.of.pred (store ((as const (Array Unicode Bool)) false) (_ Char #x23) true)))))
(simplify (str.in_re (_ char #x24) (re.of.pred (store ((as const (Array Unicode Bool)) false) (_ Char #x24) true))))

(echo "==== standard constructors ====")

(echo "== option ==")
(simplify (str.in_re "" (re.opt r)))
(simplify (str.in_re "" (re.opt (str.to_re "a"))))
(simplify (str.in_re "" (re.opt (str.to_re ""))))
(simplify (str.in_re "aba" (re.opt (str.to_re "aba"))))
(simplify (not (str.in_re "a" (re.opt (str.to_re "ab")))))
(simplify (not (str.in_re "a" (re.opt (str.to_re "b")))))

(echo "== union ==")
(simplify (str.in_re "" (re.union r (str.to_re ""))))
(simplify (str.in_re "" (re.union re.all re.none)))
(simplify (str.in_re "a" (re.union (str.to_re "a") r)))
(simplify (str.in_re "a" (re.union re.allchar re.none)))
(simplify (str.in_re "abcd" (re.union re.all (str.to_re "abcd"))))
(simplify (str.in_re "abcd" (re.union re.none (str.to_re "abcd"))))
(simplify (not (str.in_re "" (re.union re.allchar re.allchar))))
(simplify (not (str.in_re "" (re.union (str.to_re "a") (str.to_re "b")))))
(simplify (not (str.in_re "ab" (re.union (str.to_re "a") (str.to_re "b")))))

(echo "== concat ==")
(simplify (str.in_re "" (re.++ re.all (str.to_re ""))))
(simplify (str.in_re "" (re.++ (str.to_re "") (re.opt r))))
(simplify (not (str.in_re "" (re.++ (str.to_re "") re.allchar))))
(simplify (not (str.in_re "" (re.++ re.all re.empty))))
(simplify (not (str.in_re "" (re.++ (str.to_re "a") (str.to_re "")))))
(simplify (str.in_re "aba" (re.++ re.all (str.to_re "a"))))
(simplify (str.in_re "aba" (re.++ (str.to_re "aba") re.all)))
(simplify (str.in_re "aba" (re.++ re.allchar (str.to_re "ba"))))
(simplify (str.in_re "a" (re.++ (str.to_re "a") (re.opt r))))
(simplify (not (str.in_re "ba" (re.++ (str.to_re "") re.allchar))))
(simplify (not (str.in_re "a" (re.++ re.all re.empty))))
(simplify (not (str.in_re "b" (re.++ (str.to_re "a") (str.to_re "")))))

(echo "== star ==")
(simplify (str.in_re "" (re.* r)))
(simplify (str.in_re "" (re.* (str.to_re "a"))))
(simplify (str.in_re "" (re.* (str.to_re ""))))
(simplify (str.in_re "" (re.* (re.of.pred p))))
(simplify (str.in_re "aaa" (re.* (str.to_re "a"))))
(simplify (not (str.in_re "aba" (re.* (str.to_re "ab")))))
(simplify (str.in_re "aba" (re.* (str.to_re "aba"))))
(simplify (str.in_re "aba" (re.* re.allchar)))

(echo "== plus ==")
(simplify (str.in_re "" (re.+ re.all)))
(simplify (not (str.in_re "" (re.+ (str.to_re "a")))))
(simplify (str.in_re "" (re.+ (str.to_re ""))))
(simplify (str.in_re "a" (re.+ re.all)))
(simplify (str.in_re "aaaaaa" (re.+ (str.to_re "aa"))))

(echo "==== additional boolean constructors ====")

(echo "== complement ==")
(simplify (str.in_re "" (re.complement re.allchar)))
(simplify (str.in_re "" (re.complement re.empty)))
(simplify (str.in_re "" (re.complement (str.to_re "a"))))
(simplify (str.in_re "" (re.complement (re.+ (str.to_re "a")))))
(simplify (not (str.in_re "" (re.complement re.all))))
(simplify (not (str.in_re "" (re.complement (str.to_re "")))))
(simplify (not (str.in_re "" (re.complement (re.opt r)))))
(simplify (str.in_re "aba" (re.complement re.allchar)))
(simplify (str.in_re "b" (re.complement re.empty)))
(simplify (str.in_re "a" (re.complement (str.to_re ""))))
(simplify (str.in_re "a" (re.complement (str.to_re "aba"))))
(simplify (str.in_re "aba" (re.complement (re.+ (str.to_re "a")))))
(simplify (not (str.in_re "a" (re.complement re.all))))
(simplify (not (str.in_re "b" (re.complement re.allchar))))
(simplify (not (str.in_re "a" (re.complement (str.to_re "a")))))

(echo "== intersection ==")
(simplify (str.in_re "" (re.inter re.all (str.to_re ""))))
(simplify (str.in_re "" (re.inter (str.to_re "") (str.to_re ""))))
(simplify (str.in_re "" (re.inter (str.to_re "") (re.opt r))))
(simplify (not (str.in_re "" (re.inter (str.to_re "") re.allchar))))
(simplify (not (str.in_re "" (re.inter re.all (str.to_re "a")))))
(simplify (not (str.in_re "" (re.inter re.empty (str.to_re "")))))
(simplify (not (str.in_re "" (re.inter (str.to_re "a") (str.to_re "b")))))
(simplify (str.in_re "a" (re.inter re.all (str.to_re "a"))))
(simplify (str.in_re "ab" (re.inter (str.to_re "ab") (str.to_re "ab"))))
(simplify (not (str.in_re "a" (re.inter (str.to_re "") r))))
(simplify (not (str.in_re "a" (re.inter (str.to_re "") re.allchar))))
(simplify (not (str.in_re "aba" (re.inter re.all (str.to_re "a")))))
(simplify (not (str.in_re "ab" (re.inter re.empty (str.to_re "ab")))))
(simplify (not (str.in_re "c" (re.inter (str.to_re "a") (str.to_re "b")))))

(echo "== difference ==")
(simplify (str.in_re "" (re.diff (str.to_re "") re.allchar)))
(simplify (str.in_re "" (re.diff (re.opt r) re.empty)))
(simplify (str.in_re "a" (re.diff (str.to_re "a") (str.to_re "b"))))
(simplify (str.in_re "ab" (re.diff (str.to_re "ab") re.none)))
(simplify (str.in_re "ba" (re.diff re.all re.allchar)))
(simplify (not (str.in_re "" (re.diff r r))))
(simplify (not (str.in_re "" (re.diff (str.to_re "") re.all))))
(simplify (not (str.in_re "" (re.diff (str.to_re "a") (str.to_re "a") ))))
(simplify (not (str.in_re "a" (re.diff re.allchar (str.to_re "a")))))
(simplify (not (str.in_re "b" (re.diff re.all re.allchar))))
(simplify (not (str.in_re "ab" (re.diff re.allchar (str.to_re "a")))))

(echo "==== counting loops ====")

(echo "== between m and n times ==")
(simplify (str.in_re "" ((_ re.loop 0 10) r)))
(simplify (str.in_re "" ((_ re.loop 1 3) (re.opt r))))
(simplify (not (str.in_re "" ((_ re.loop 1 3) (str.to_re "a")))))
(simplify (not (str.in_re "" ((_ re.loop 1 0) (str.to_re "b")))))
(simplify (str.in_re "aa" ((_ re.loop 1 3) (str.to_re "a"))))
(simplify (str.in_re "bb" ((_ re.loop 0 2) (str.to_re "b"))))
(simplify (str.in_re "abab" ((_ re.loop 2 4) (str.to_re "ab"))))
(simplify (str.in_re "aba" ((_ re.loop 3 3) re.allchar)))
(simplify (not (str.in_re "a" ((_ re.loop 0 0) r))))
(simplify (not (str.in_re "ab" ((_ re.loop 1 3) (str.to_re "a")))))
(simplify (not (str.in_re "b" ((_ re.loop 1 0) (str.to_re "b")))))
(simplify (not (str.in_re "aaa" ((_ re.loop 1 2) (str.to_re "a")))))

(echo "== at least m times ==")
(simplify (str.in_re "" ((_ re.loop 0) r)))
(simplify (str.in_re "" ((_ re.loop 0) re.all)))
(simplify (str.in_re "" ((_ re.loop 2) re.all)))
(simplify (not (str.in_re "" ((_ re.loop 2) re.allchar))))
(simplify (not (str.in_re "" ((_ re.loop 3) (str.to_re "a")))))
(simplify (str.in_re "a" ((_ re.loop 0) re.all)))
(simplify (str.in_re "aba" ((_ re.loop 3) re.all)))
(simplify (str.in_re "aa" ((_ re.loop 0) (str.to_re "aa"))))
(simplify (str.in_re "aa" ((_ re.loop 2) (str.to_re "a"))))
(simplify (not (str.in_re "aa" ((_ re.loop 3) re.allchar))))

(echo "== exactly m times ==")
(simplify (str.in_re "" ((_ re.^ 0) r)))
(simplify (not (str.in_re "a" ((_ re.^ 0) r))))
(simplify (str.in_re "" ((_ re.^ 0) re.allchar)))
(simplify (str.in_re "" ((_ re.^ 1) (str.to_re ""))))
(simplify (str.in_re "a" ((_ re.^ 1) re.allchar)))
(simplify (str.in_re "" ((_ re.^ 2) (str.to_re ""))))
(simplify (not (str.in_re "a" ((_ re.^ 2) (str.to_re "")))))
(simplify (not (str.in_re "a" ((_ re.^ 2) re.allchar))))

(echo "==== other extensions ====")

(echo "== if-then-else ==")
(simplify (str.in_re "" (ite b1 (str.to_re "") (str.to_re ""))))
(simplify (str.in_re "a" (ite b1 (str.to_re "a") re.allchar)))
(simplify (str.in_re "" (ite b1 re.all (str.to_re ""))))
(simplify (not (str.in_re "" (ite b1 re.allchar (re.++ (str.to_re "a") re.all)))))
(simplify (not (str.in_re "abc" (ite b1 re.allchar (str.to_re "cba")))))
(simplify (str.in_re "" (ite true (str.to_re "") (str.to_re "a"))))
(simplify (str.in_re "a" (ite true re.allchar (str.to_re "b"))))
(simplify (not (str.in_re "" (ite false re.all (str.to_re "b")))))
(simplify (not (str.in_re "a" (ite false re.allchar (str.to_re "b")))))

(echo "== reverse ==")
(simplify (str.in_re "" (re.reverse (str.to_re ""))))
(simplify (str.in_re "a" (re.reverse (str.to_re "a"))))
(simplify (str.in_re "abb" (re.reverse (str.to_re "bba"))))
(simplify (not (str.in_re "ab" (re.reverse (str.to_re "ab")))))
(simplify (str.in_re "ab" (re.reverse (re.++ re.allchar (str.to_re "a")))))
(simplify (str.in_re "abc" (re.reverse re.all)))
(simplify (not (str.in_re "abc" (re.reverse re.allchar))))
(simplify (not (str.in_re "abc" (re.reverse re.none))))

(echo "== derivative ==")
(simplify (str.in_re "abc" (re.derivative c1 re.all)))
(simplify (str.in_re "" (re.derivative c1 (str.to_re (seq.unit c1)))))
(simplify (str.in_re "" (re.derivative c1 (re.opt (str.to_re (seq.unit c1))))))
(simplify (str.in_re "" (re.derivative c1 (re.* (str.to_re (seq.unit c1))))))
(simplify (str.in_re "" (re.derivative c1 (re.+ (str.to_re (seq.unit c1))))))
(simplify (not (str.in_re "" (re.derivative c1 (re.++ (str.to_re (seq.unit c1)) (str.to_re (seq.unit c1)))))))
(simplify (str.in_re "" (re.derivative c1 (re.++ (str.to_re (seq.unit c1)) (str.to_re "")))))
(simplify (not (str.in_re (seq.unit c1) (re.derivative c1 (re.++ (str.to_re (seq.unit c1)) (str.to_re ""))))))
(simplify (not (str.in_re (seq.unit c1) (re.derivative c1 re.none))))

(echo "==== complex combinations ====")

(simplify (str.in_re "aaaaaaa" (re.+ (re.union (str.to_re "aa") (str.to_re "aaa")))))
(simplify (not (str.in_re "aaaaaaa" (re.+ (re.union (str.to_re "aaa") (str.to_re "aaaaa"))))))
(simplify (str.in.re "aaabbb" (re.reverse (re.++ (re.+ (str.to_re "b")) (re.* re.allchar)))))
(simplify (not (str.in.re "abc" (re.reverse (re.++ (re.+ (str.to_re "b")) (re.* re.allchar))))))

(echo "==== symbolic test cases ====")

(echo "== symbolic string ==")
(simplify (str.in_re x (re.* re.allchar)))
(simplify (str.in_re x (str.to_re x)))
(simplify (not (str.in_re x re.none)))

(echo "== if-then-else with unknown condition ==")
(simplify (str.in_re "a" (ite (= x "a") (str.to_re "a") re.allchar)))
(simplify (str.in_re "a" (re.* (ite (= x "a") (str.to_re "a") re.allchar))))
(simplify (str.in_re x (re.+ (ite (= y "a") (re.* re.allchar) re.all))))
(simplify (str.in_re x (re.* (ite (= y "a") re.allchar re.all))))

(echo "== left/right derivatives with symbolic string ==")

(simplify (str.in_re (str.++ "a" x) (re.++ re.allchar re.all)))
(simplify (str.in_re (str.++ x "a") (re.++ re.all re.allchar)))
(simplify (str.in_re (str.++ "abc" x) (re.++ (str.to_re "abc") (re.* re.allchar) )))
(simplify (str.in_re (str.++ x "abc") (re.++ (re.* re.allchar) (str.to_re "abc"))))
(simplify (str.in_re (str.++ "aa" x) (re.++ (re.+ (str.to_re "a")) re.all)))
(simplify (str.in_re (str.++ x "aa") (re.++ re.all (re.+ (str.to_re "a")))))
(simplify (not (str.in_re (str.++ x "b") (re.++ re.allchar (str.to_re "a")))))
(simplify (not (str.in_re (str.++ "b" x) (re.++ (str.to_re "a") re.allchar))))

(echo "==== Complex complement examples ====")

(simplify (str.in_re "" (re.comp (re.++ (re.++ re.all (str.to_re "a")) ((_ re.^ 100000) re.allchar)))))
(simplify (str.in_re "abcde" (re.comp (re.++ (re.++ re.all (str.to_re "a")) ((_ re.^ 100000) re.allchar)))))
(simplify (not (str.in_re "babbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb" (re.comp (re.++ (re.++ re.all (str.to_re "a")) ((_ re.^ 100) re.allchar))))))

(echo "==== evil regex matching example ====")

(simplify (not (str.in_re "the quick brown fox jumps over the lazy dog" (re.++ (re.++ (re.+ (re.++ (re.+ (re.range (_ char #x1) (_ char #x7F))) re.allchar)) (str.to_re (_ char #x0))) (re.+ (re.range (_ char #x1) (_ char #x7F)))))))
